es:event_system{i:l}, e1,e2:es-E(es), P:({e:es-E(es)| 
es:event_system{i:l}, e1,e2:es-E(es), P:({(loc(e) = loc(e1)  Id)  ((es-first(es; e)))} 
es:event_system{i:l}, e1,e2:es-E(es), P:(prop{i:l}).
(loc(e2) = loc(e1)  Id)  (e(e1,e2].P(e)  prop{i:l}) 

latex

Definitions	guard(T), sq_type(T), A c B, P  Q, es-le(es; e; e'), es-locl(es; e; e'), x(s), e(e1,e2].P(e), t  T, P  Q, prop{i:l}, P  Q, x:A. B(x), P  Q
Lemmas	event system wf, es-E wf, es-first wf, assert wf, not wf, es-locl-iff, es-le-loc, Id sq, es-locl wf, es-causl wf, es-loc wf, Id wf